/*
 * DIMACSParser.cpp
 *
 * Copyright 2012 Fabian Wenzelmann
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

#include "bfr/DIMACSParser.hpp"

#include <iostream>
#include <string>

#include <boost/lexical_cast.hpp>

#include "bfr/Literal.hpp"

namespace bfr {

// TODO: I think we need some more range checking for the parse methods
// to catch all errors
DIMACSParser::DIMACSParser()
	: variableCount(0), clauseCount(-1),
	  clauses(0), type(DIMACSParser::problem_type::UNKNOWN){ }

DIMACSParser::~DIMACSParser() { }

const char DIMACSParser::COMMENT_CHAR = 'c';
const char DIMACSParser::PROBLEM_CHAR = 'p';

const char DIMACSParser::CNF_PROBLEM[] = "cnf";

const char DIMACSParser::MINUS = '-';

bool DIMACSParser::isLineEmpty(const std::string &line) const {
    return (line.find_first_not_of(" \t") == std::string::npos);
}

ClauseSet* DIMACSParser::parse(std::istream &in) throw(std::string) {
	std::string line;
	if (!in.good()) {
	    throw std::string("Can't parse DIMACS DNF from stream.");
	}
	do {
	    getline(in, line);
	    if (in.eof()) {
	        throw std::string("Can't parse DIMACS DNF from stream.");
	    }
	} while ((line[0] == COMMENT_CHAR) || isLineEmpty(line));


	// now expecting the comment line
	if ((line.size() == 0) || (line[0] != PROBLEM_CHAR)) {
	    throw std::string("Missing problem line in DIMACS input.");
	}
        try {
            readProblemLine(line);
        }
        catch (std::string &e) {
            throw e;
        }

        for (size_t i = 0; i < clauseCount;) {
            if (in.eof()) {
                throw std::string("Input does not define as many clauses as "
                        "defined in problem line.");
                delete clauses;
            }
            getline(in, line);
            if ((line.size() == 0) || (line[0] == COMMENT_CHAR)) {
                continue;
            }
            try {
                    Clause *clause = readClause(line);
                    clauses->addSecure(clause);
                    i++;
                }
                catch (std::string &e) {
                    delete clauses;
                    throw e;
                }
        }
	return clauses;
}

size_t DIMACSParser::parseNumber(std::string &line, size_t *pos) throw(std::string) {
	// search for the next space that terminates the number
	size_t nextSpace = line.find(' ', *pos);
	if (nextSpace == std::string::npos) {
		// there is no " ". So we assume the the rest of the
		// line is the whole number
		nextSpace = line.size();
	}
	// get the substring
	size_t len = nextSpace - *pos;
	std::string substr = line.substr(*pos, len);
	try {
		*pos = nextSpace + 1;
		return boost::lexical_cast<size_t>( substr );
	}
	catch (const boost::bad_lexical_cast &e ) {
		throw std::string("Can't parse ") + substr + " as number.";
	}
}

void DIMACSParser::readProblemLine(std::string &line) throw(std::string) {
	// we know that the line starts with "p"
	// find the first pos where we expect the variable number

	if (line.size() <= 3) {
	    throw std::string("Expected \"p PROBLEM_INSTANCE (aka cnf)\"."
	   			   "But found only \"" + line + "\".");
	}

	if (line[1] != ' ') {
		throw std::string("Expected BLANK after \"p\", but found \"p")
			+ line[1] +std::string("\".");
	}

	size_t pos = 2;
	// assume that now we have
	// "PROBLEM_TYPE VARIABLES CLAUSES"

	// find the next whitespace starting at pos 2 (end of the problem type)
	size_t nextSpace = line.find(' ', pos);
	// get the substring
	std::string problemType = line.substr(pos, nextSpace - pos);
	// set the global type
	if (problemType.compare(DIMACSParser::CNF_PROBLEM) == 0) {
		type = DIMACSParser::problem_type::CNF;
	}
	else {
		type = DIMACSParser::problem_type::UNKNOWN;
	}
	// move from space to next char
	pos = nextSpace + 1;
	try {
		variableCount = parseNumber(line, &pos);
		clauseCount = parseNumber(line, &pos);
		clauses = new ClauseSet(clauseCount);
	}
	catch(std::string &e) {
		throw e;
	}
}

Clause* DIMACSParser::readClause(std::string &line) throw(std::string) {
    Clause *clause = new Clause();

    size_t pos = 0;
    size_t id = -1;
    // read clauses until we have "0"
    do {
        bool polarity = true;
        if (line[pos] == DIMACSParser::MINUS) {
            polarity = false;
            pos++;
        }
        try {
            id = parseNumber(line, &pos);
            if (id != 0) {
                clause->add(Literal(id - 1, polarity));
            }
        }
        catch (const std::string &str) {
            delete clause;
            throw str;
        }
    } while (id != 0);

    return clause;
}

size_t DIMACSParser::getVariableCount() const {
    return variableCount;
}

}


